\newcommand{\encoding}[1]{\llbracket #1 \rrbracket}
\newcommand{\pass}[2]{\til{#1} \{ #2 \}}

%\newpage
The decidability of termination in \hof 
presented in Section \ref{s:wsts}
provides compelling evidence 
on the fact that the limited forwarding %communication 
entails a loss of expressive power for \hocore.
It is therefore worth 
investigating alternatives for 
recovering such an expressive power while preserving the essence of limited forwarding. 

In this section we examine one such alternatives.
We analyze the consequences of extending \hof with a \emph{passivation} construct, 
an operator that allows to \emph{suspend}
the execution of a process at run time. 
As such, it comes in handy to represent scenarios of (dynamic) system reconfiguration, 
which are often indispensable 
in the specification of 
open, extensible systems such as component-based ones. 
Passivation has been considered by higher-order calculi such as the Kell calculus \citep{SchmittS04} and Homer \citep{HilBun04}, 
and finds several applications (see, e.g., \citep{BundgaardGHHN08}). 
Here we shall consider a passivation construct of the form
%Hence, we have the construct 
$\pass{a}{P}$, which represents a \emph{passivation unit} named $a$ that contains a process $P$.
The passivation unit is a \emph{transparent locality}, in that 
there are no restrictions on the interactions between $P$ 
and processes surrounding $a$. 
The execution of $P$ can be \emph{passivated}
at an arbitrary time; this is represented by the evolution of 
$\pass{a}{P}$ into the nil process by means of an output action $\Ho{a}{P}$.
Hence, the passivation of $\pass{a}{P}$ process might lead to a synchronization with any interacting input action on $a$.
%in which $P$ can no longer evolve.

We consider \hopf, the extension of \hof with a passivation construct as described above.
The syntax extends as expected; 
for the sake of consistency, we notice that the process $P$ in $\pass{a}{P}$ 
respects the limitation on the shape of 
output objects introduced for \hof.
The LTS for \hopf is the same as that for \hof in Section \ref{s:lang}, extended with the two following rules 
which formalize the intuitions given before with respect to transparent localities and passivation, respectively:

\[
 \frac{P \xrightarrow{~\alpha~} P'}{\pass{a}{P}  \xrightarrow{~\alpha~} \pass{a}{P'}} ~~\textsc{Loc}
\qquad 
 \pass{a}{P} \arr{~\Ho{a}{P}~}  \nil ~~\textsc{Pas} \, .
\]



\subsection{A Faithful Encoding of Minsky Machines into \hopf}
Here we investigate the expressiveness of \hopf by exhibiting 
an encoding of Minsky machines into \hopf. 
Interestingly, unlike the encoding presented in Section \ref{s:turing},
the encoding into \hopf is \emph{faithful}. %\footnote{In fact, the encoding is \emph{nearly-deterministic}, because of the encoding of replication we are considering.}.
As such, in \hopf \emph{both} termination and convergence are \emph{undecidable} problems. 
Hence, it is fair to say that the passivation construct ---even with the limitation on the shape of (output) processes--- allows to recover the expressive power lost in restricting \hocore as \hof. 





The encoding is given in Figure \ref{t:encod-pas}; we now give some intuitions on it. 
A register $k$ with value $m$ is represented by a passivation unit $r_k$ that contains 
the encoding of number $m$, denoted $\encn{m}{k}$. 
In turn, $\encn{m}{k}$ consists of a chain of $m$ nested input prefixes on name $u_k$; 
it also contains other prefixes on $a_1$ and $a_2$ which are used for synchronization purposes during the execution of instructions. 
The encoding of zero is given by an input action on $z_k$ that prefixes a trigger $\outC{a_z}$.

\begin{figure}[t] 
\centering  
{%\small 
\begin{tabular}{l}   
\(  
\mathrm{\textsc{Register}}~r_k \qquad
\encp{r_k = n}{\mms}   =  \pass{r_k}{\encn{n}{k}} 
\) \\ %where

\quad where \\

\quad \quad \quad  \(  
\encn{n}{k}=\left\{  
\begin{array}{ll}  
 z_k.\overline{a_z}  & \textrm{if } n= 0 \\  
 u_k.(\overline{a_1} \parallel a_2.\encn{n-1}{k}) ~~& \textrm{if } n> 0 .  
\end{array}\right.  
\)

% \(
% \begin{array}{l}
%  \qquad \encn{0}{k}  =  z_k.\overline{a_z} \quad \quad   
% \encn{n}{k}  =  u_k.(\overline{a_1} \parallel a_2.\encn{n-1}{k}) ~~~\mbox{if $n>0$}\\
% %\qquad \quad M_k  =  !i_k.r_k(x).(\Ho{c}{x} \parallel \pass{h_k}{c(y).u_k.(\overline{a_1} \parallel a_2.y) } )
% \end{array}
% 
% \)\\  
\\ \\ 


\(
\begin{array}{lll}   
\multicolumn{3}{l}{\mathrm{\textsc{Instructions}}~(i:I_i)}\\  
\encp{(i: \mathtt{INC}(r_k))}{\mms}&  = &  !p_i.( r_k(x).(\Ho{c_k}{x} \parallel \pass{r_k}{c_k(y).(\outC{a_p} \parallel u_k.(\overline{a_1} \parallel a_2.y)) } \parallel  a_p.\overline{p_{i+1}}))\\
\encp{(i: \mathtt{DECJ}(r_k,s))}{\mms}&  = & \quad !p_i.( m(x).x \\
& &  \qquad \quad \parallel \pass{d}{\overline{u_k} \parallel a_1.\Ho{m}{s(x).d(x).(\overline{a_2} \parallel \overline{p_{i+1}})}} \\
& &  \qquad \quad \parallel \pass{s}{\overline{z_k} \parallel a_z.\Ho{m}{d(x).s(x).r_k(t).(\pass{r_k}{z_k.\overline{a_z}}\parallel \overline{p_s})}})  
\end{array}   
\) \\ \\

\end{tabular}
}  
\caption{Encoding of Minsky machines into \hopf.}  
\label{t:encod-pas}  
%\vspace{-5mm}
\end{figure}

As expected, the encoding of an increment operation on the value of register $k$ 
consists in the enlargement of the chain of nested input prefixes it contains.
For that purpose, the content of passivation unit $r_k$ is obtained with an input on $r_k$.
We therefore need to recreate the passivation unit $r_k$ with the encoding of the incremented value.
Notice that we require an additional synchronization on $c_k$ in order to ``inject'' 
such a previous content in a new passivation unit called $r_k$.
This way, the  chain of nested inputs in $r_k$ can be enlarged while
respecting the limitation on the shape of processes inside passivation units.
%Once this has taken place, %e previous content has been injected into the new copy of $r_k$, 
As a result, the chain is enlarged by putting it behind some prefixes, and 
the next instruction can be invoked. 
This is done by a synchronization on name $a_p$.

The encoding of a decrement of the value of register $k$
consists of an internal, exclusive choice implemented as two passivation units that execute in parallel:
the first one, named $d$, implements the behavior for decrementing the value of a register,
while the second one, named $s$, implements the behavior for performing the jump to some given instruction.
Unlike the encoding of Minsky machines in \hof presented in Section \ref{s:turing}, 
this internal choice %implemented by these two passivation units 
behaves faithfully with respect to the encoding instruction, i.e.,
the behavior inside $d$ will only execute if the value in $r_k$ is greater than zero, 
whereas the behavior inside $s$ will only execute if that value is equal to zero.
It is indeed a deterministic choice in that it is \emph{not} the case that both an
input prefix on $u_k$  (which triggers the ``decrement branch'' defined by $d$)
and one on $z_k$ (which triggers the ``jump branch'' defined by $s$)
are available at the same time; this is because of the way in which we encode numbers, i.e., as  a chain of input prefixes.
In addition to the passivation units, the
encoding of decrement features a ``manager''
(implemented as a synchronization on $m$) 
that enables the behavior of the chosen passivation unit 
by placing it at the top-level, 
and consumes both $s$ and $d$ afterwards, thus
leaving no residual processes after performing the instruction.
In case the value of the register is equal to some $n > 0$, then a decrement is implemented
by consuming the input prefixes on $u_k$ and $a_2$ and the output prefix on $a_1$ through
suitable synchronizations. It is worth noticing that these synchronizatons 
are only possible because the passivation units containing the encoding of $n$ behave as 
transparent localities, and hence able to interact with its surrounding context.
As a result, the encoding of $n-1$ remains inside $r_k$
and the next instruction is invoked. In case the value of the register is equal to zero, 
the passivation unit $r_k$ is consumed and recreated with the encoding of zero inside.
The jump is then performed by invoking the respective instruction.

We are now ready to define the encoding of a configuration of a Minsky machine into \hopf.

\begin{mydefi}[Encoding of Configurations]\label{d:conf-mm-pas}  
Let $N$ be a \mma with registers $r_0 = m_0$, $r_1=m_1$ and instructions  
$(1:I_1), \ldots, (n:I_n)$.  
The encoding of a configuration $(i, m_0, m_1)$ of $N$
into \hopf is defined by the encodings in Figure \ref{t:encod-pas} as 
\begin{equation*}  
\encp{(i, m_0, m_1) }{\mms} = \overline{p_i} \parallel \encp{r_0 = m_0}{\mms} \parallel \encp{r_1 = m_1}{\mms} \parallel   \prod^{n}_{i=1} \encp{(i:I_i)}{\mms} \, ,
\end{equation*}  
%for which we assume 
assuming 
fresh, pairwise different names $r_j$, $u_k$, $z_k$, $p_1, \ldots, p_n$, %$inc_j$, $dec_j$, $ack$ 
(for $j \in \{0,1\}$).
\end{mydefi}  


\subsection{Correctness of the Encoding}
We divide the proof of correctness into two properties:
completeness (Lemma \ref{l:compl-pas}) and soundness (Lemma \ref{l:sound-pas}).

\begin{lemma}[Completeness]\label{l:compl-pas}
 Let $(i, m_0, m_1)$ be a configuration of a \mma $N$. Then, 
%\begin{enumerate}
% \item If $(i, m_0, m_1)\nrightarrow$  then $\encp{(i, m_0, m_1) }{\mms} \nrightarrow$
% \item If 
if $(i, m_0, m_1)\minskred (i', m_0', m_1')$ then, for some finite $j$ and a process $P$, 
it holds that $\encp{(i, m_0, m_1) }{\mms} \pired^j P \equiv \encp{(i', m_0', m_1') }{\mms}$.
%\end{enumerate}
\end{lemma}

\begin{proof}
We proceed by a case analysis on the instruction  performed by the \mma.
Hence, we distinguish three cases corresponding to the behaviors associated to rules
\textsc{M-Inc}, \textsc{M-Dec}, and \textsc{M-Jmp}.
Without loss of generality, we restrict our analysis to operations on register $r_0$.

\begin{description}
 \item[Case \textsc{M-Inc}:] We have a Minsky configuration $(i, m_0, m_1)$ with 
$(i: \mathtt{INC}(r_0))$. By Definition \ref{d:conf-mm-pas}, its encoding into \hof with passivation is as follows:
\begin{eqnarray*}
\encp{(i, m_0, m_1)}{\mms} & = &   \overline{p_i} \parallel \encp{r_0 = m_0}{\mms} \parallel \encp{r_1 = m_1}{\mms} \parallel  \\
& & \encp{(i: \mathtt{INC}(r_0))}{\mms} \parallel   \prod_{l=1..n,l\not = i} \encp{(l:I_l)}{\mms} 
%p_i.( r_0(x).(\Ho{c_0}{x} \parallel \pass{r_0}{c_0(y).(\outC{a_p} \parallel u_0.(\overline{a_1} \parallel a_2.y)) } \parallel  a_p.\overline{p_{i+1}})) \\
%& & \parallel \encp{r_1 = m_1}{\mms} \parallel   \prod^{n}_{i=1} \encp{(i:I_i)}{\mms}
\end{eqnarray*}


After consuming the program counter $p_i$  we have the following 
\begin{eqnarray*}
\encp{(i, m_0, m_1)}{\mms}&  \pired & \pass{r_0}{\encn{m_0}{0}} \parallel r_0(x).(\Ho{c_0}{x} \parallel \pass{r_0}{c_0(y).(\outC{a_p} \parallel u_0.(\overline{a_1} \parallel a_2.y)) } )\parallel  \\
& & a_p.\overline{p_{i+1}} \parallel S = P_1
\end{eqnarray*}
where $S = \encp{r_1 = m_1}{\mms} \parallel \prod_{i=1}^n \encp{(i:I_i)}{\mms}$ stands for the rest of the system.
The only reduction possible at this point is the synchronization on $r_0$, which allows 
the content of the passivation unit $r_0$ to be communicated:
\[
 P_1 \pired \Ho{c_0}{\encn{m_0}{0}} \parallel \pass{r_0}{c_0(y).(\outC{a_p} \parallel u_0.(\overline{a_1} \parallel a_2.y)) } \parallel  a_p.\overline{p_{i+1}} \parallel S = P_2 \, .
\]
Now there is a synchronization on $c_0$, which allows to ``inject'' the encoding of value $m_0$ inside the passivation unit $r_0$ respecting the limitation of the language:
\[
 P_2 \pired  \pass{r_0}{(\outC{a_p} \parallel u_0.(\overline{a_1} \parallel a_2.\encn{m_0}{0})) } \parallel  a_p.\overline{p_{i+1}} \parallel S = P_3 \, .
\]
The only possible synchronization from $P_3$ is the one on $a_p$, which 
works as an acknowledgment signal, and allows to release the program counter 
for instruction $i+1$. By performing such a synchronization, and by the encoding of numbers, we obtain the following
\[
 P_3 \pired \pass{r_0}{\encn{m_0 +1}{0}} \parallel \overline{p_{i+1}} \parallel S = P_4
\]
It is then easy to see that $P_4 \equiv \encp{(i+1, m_0+1, m_1)}{\mms}$, as desired. 


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\item[Case \textsc{M-Dec}:] We have a Minsky configuration $(i, c, m_1)$ with 
$c > 0$ and 
$(i: \mathtt{DEC}(r_0,s))$. By Definition \ref{d:conf-mm-pas}, its encoding into \hof with passivation is as follows:
\begin{eqnarray*}
\encp{(i, c, m_1)}{\mms} & = &   \overline{p_i} \parallel \encp{r_0 = c}{\mms} \parallel \encp{r_1 = m_1}{\mms} \parallel  \\
& & \encp{(i: \mathtt{DEC}(r_0,s))}{\mms} \parallel   \prod_{l=1..n,l\not = i} \encp{(l:I_l)}{\mms} 
\end{eqnarray*}
We begin by consuming the program counter $p_i$, which leaves the content of $\encp{(i: \mathtt{DEC}(r_0,s))}{\mms}$ exposed.
Using the encoding of numbers we have the following:
\begin{eqnarray*}
 \encp{(i, c, m_1)}{\mms} & \pired & \pass{r_0}{u_0.(\overline{a_1} \parallel a_2.\encn{c-1}{0})} \parallel m(x).x \parallel \\
& &   \pass{d}{\overline{u_0} \parallel a_1.\Ho{m}{s(x).d(x).(\overline{a_2} \parallel \overline{p_{i+1}})}} \parallel \\
& &   \pass{s}{\overline{z_0} \parallel a_z.\Ho{m}{d(x).s(x).r_0(t).(\pass{r_0}{z_0.\overline{a_z}}\parallel \overline{p_s})}} \parallel S = P_1
\end{eqnarray*}
where $S = \encp{r_1 = m_1}{\mms} \parallel \prod_{i=1}^n \encp{(i:I_i)}{\mms}$ stands for the rest of the system.
Notice that only reduction possible at this point is the synchronization on $u_0$, 
which signals the fact we are performing a decrement instruction.
Such a synchronization enables one on $a_1$. After these two synchronizations we have 
\begin{eqnarray*}
 P_1 & \pired^2 & \pass{r_0}{a_2.\encn{c-1}{0}} \parallel m(x).x \parallel \pass{d}{\Ho{m}{s(x).d(x).(\overline{a_2} \parallel \overline{p_{i+1}})}} \parallel \\
& &   \pass{s}{\overline{z_0} \parallel a_z.\Ho{m}{d(x).s(x).r_0(t).(\pass{r_0}{z_0.\overline{a_z}}\parallel \overline{p_s})}} \parallel S = P_2 \, .
\end{eqnarray*}

Starting in $P_2$ the only reduction possible is due to the synchronization on $m$, which gives us the following:
\begin{eqnarray*}
 P_2 & \pired & \pass{r_0}{a_2.\encn{c-1}{0}} \parallel s(x).d(x).(\overline{a_2} \parallel \overline{p_{i+1}}) \parallel \pass{d}{\nil} \parallel \\
& &   \pass{s}{\overline{z_0} \parallel a_z.\Ho{m}{d(x).s(x).r_0(t).(\pass{r_0}{z_0.\overline{a_z}}\parallel \overline{p_s})}} \parallel S = P_3 \, .
\end{eqnarray*}
In $P_3$ we have that passivation units $s$ and $d$ are consumed, thus we have:
\[
 P_3  \pired  \pass{r_0}{a_2.\encn{c-1}{0}} \parallel \overline{a_2} \parallel \overline{p_{i+1}} \parallel S = P_4 \, .
\]
At this point it is easy to see that, after a synchronization on $a_2$, we obtain
\[
 P_4 \pired \equiv  \encp{(i+1, c-1, m_1)}{\mms} 
\]
as desired.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\item[Case \textsc{M-Jmp}:] We have a Minsky configuration $(i, 0, m_1)$ and 
$(i: \mathtt{DEC}(r_0,s))$. By Definition \ref{d:conf-mm-pas}, 
its encoding into \hof with passivation is as follows:
\begin{eqnarray*}
\encp{(i, 0, m_1)}{\mms} & = &   \overline{p_i} \parallel \encp{r_0 = 0}{\mms} \parallel \encp{r_1 = m_1}{\mms} \parallel  \\
& & \encp{(i: \mathtt{DEC}(r_0,s))}{\mms} \parallel   \prod_{l=1..n,l\not = i} \encp{(l:I_l)}{\mms} \, .
\end{eqnarray*}
We begin by consuming the program counter $p_i$, which leaves the content of $\encp{(i: \mathtt{DEC}(r_0,s))}{\mms}$ exposed.
Using the encoding of numbers we have the following:
\begin{eqnarray*}
 \encp{(i, 0, m_1)}{\mms} & \pired & \pass{r_0}{z_0.a_z} \parallel m(x).x \parallel \\
& &   \pass{d}{\overline{u_0} \parallel a_1.\Ho{m}{s(x).d(x).(\overline{a_2} \parallel \overline{p_{i+1}})}} \parallel \\
& &   \pass{s}{\overline{z_0} \parallel a_z.\Ho{m}{d(x).s(x).r_0(t).(\pass{r_0}{z_0.\overline{a_z}}\parallel \overline{p_s})}} \parallel S = P_1 
\end{eqnarray*}
where $S = \encp{r_1 = m_1}{\mms} \parallel \prod_{i=1}^n \encp{(i:I_i)}{\mms}$ stands for the rest of the system.
In $P_1$, the only reduction possible is through a synchronization on $z_0$, 
which signals the fact we are performing a jump.
Such a synchronization, in turn, enables one on $a_z$.
We then have:
\begin{eqnarray*}
P_1 & \pired^2 & \pass{r_0}{\nil} \parallel m(x).x \parallel \\
& &   \pass{d}{\overline{u_0} \parallel a_1.\Ho{m}{s(x).d(x).(\overline{a_2} \parallel \overline{p_{i+1}})}} \parallel \\
& &   \pass{s}{\Ho{m}{d(x).s(x).r_0(t).(\pass{r_0}{z_0.\overline{a_z}}\parallel \overline{p_s})}} \parallel S = P_2 \, .
\end{eqnarray*}
The only possible reduction from $P_2$ is by means of a synchronization on $m$.
This gives us:
\begin{eqnarray*}
P_2 & \pired & \pass{r_0}{\nil} \parallel d(x).s(x).r_0(t).(\pass{r_0}{z_0.\overline{a_z}}\parallel \overline{p_s}) \parallel \\
& &   \pass{d}{\overline{u_0} \parallel a_1.\Ho{m}{s(x).d(x).(\overline{a_2} \parallel \overline{p_{i+1}})}} \parallel \pass{s}{\nil} \parallel S = P_3 \, .
\end{eqnarray*}
In $P_3$ the two passivation units on $d$ and $s$ are consumed, which gives us:
\[
 P_3  \pired  \pass{r_0}{\nil} \parallel r_0(t).(\pass{r_0}{z_0.\overline{a_z}}\parallel \overline{p_s}) \parallel S = P_4 \, .
\]
At this point, it is easy to see that after a synchronization on $r_0$ we obtain:
\[
 P_4 \pired \equiv \encp{(s, 0, m_1)}{\mms} 
\]
as desired.
\end{description}
% \qed
\end{proof}

\begin{lemma}[Soundness]\label{l:sound-pas} 
Let $(i,m_0,m_1)$ be a configuration of a Minsky machine $N$. \\  %Consider a process $P = $.
If $\encp{(i,m_0,m_1)}{\mms}  \pired P_1$ then for every computation of $P_1$ there 
exists a $P_j$ such that 
%\begin{enumerate}
%\item $P_1 \pired \cdots \pired P_j$ 
%\item 
$P_j = \encp{(i',m'_0,m'_1)}{\mms}$ and
%\item 
$(i,m_0,m_1)\minskred (i',m'_0,m'_1)$.
%\end{enumerate}
\end{lemma}
 
\begin{proof}
Consider the reduction  $\encp{(i,m_0,m_1)}{\mms}  \pired P_1$. An analysis of the structure of process
 $\encp{(i,m_0,m_1)}{\mms}$ reveals that, in all cases, the only possibility for the first step corresponds to the
consumption of the program counter $p_i$. This implies that there exists an instruction
labeled with $i$, that can be executed from the configuration $(i,m_0,m_1)$.
%That is, there exists a configuration  $(i',m'_0,m'_1)$ such that  $(i,m_0,m_1) \minskred (i',m'_0,m'_1)$.
We proceed by a case analysis on the possible instruction, considering also the 
fact that the register on which the instruction acts can hold a value equal or greater than zero.

In all cases, it can be shown that computation evolves %(nearly) 
deterministically
until reaching a process in which a new program counter (that is, some $\overline{p_{i'}}$) appears.
%To be precise, there is 
%some non-determinism associated with the unfoldings of the encoding of recursive definitions
%(see Lemma \ref{l:corr-repl}).
%Since recursion is guarded, each recursive definition can be unfolded at most once, thus introducing at most a finite
%number of additional reductions. 
The program counter $\overline{p_{i'}}$ is always inside a process that corresponds to $\encp{(i',m'_0,m'_1)}{\mms}$,
where $(i,m_0,m_1)\minskred (i',m'_0,m'_1)$. 
The detailed analysis follows the same lines as the one reported for the proof of Lemma \ref{l:compl-pas}, and we omit it.
% \qed
\end{proof}

\begin{corollary}\label{l:terminate}
Let $N$ be a Minsky machine. We have that $N \nrightarrow_{M}$ if and only if $\encp{N}{\mms} \nrightarrow$.
\end{corollary}

\begin{proof}
Straightforward from Lemmas \ref{l:compl-pas} and \ref{l:sound-pas}.
% \qed
\end{proof}

\begin{lemma}
Termination and convergence are undecidable in \hopf.
\end{lemma}

\begin{proof}
 This is an immediate consequence of previous results (Lemmas \ref{l:compl-pas} and \ref{l:sound-pas}, Corollary \ref{l:terminate}).% \qed
\end{proof}

